1.
msc diagrams: three_way_teardown1(19) and three_way_teardown2(16)
INCONSISTENCY:
Matching formula: m19 = k16
Precondition 1: rel (m19 , n19 , three_wayconnected k19); Precondition 2: rel (m16 , n16 , three_wayconnected k16);
Post condition 1: rel (n19 , k19 , connected); Post condition 2: state (m16 , dial) & state (n16 , dial);

2.
msc diagrams: three_way_teardown1(19) and call_setup_failure2(9)
INCONSISTENCY:
Matching formula: m19 = m9
Precondition 1: rel (m19 , n19 , three_wayconnected k19);
Precondition 2: state (m9 , ringing n9);
Post condition 1: rel (n19 , k19 , connected);
Post condition 2: state (n9 , idle);

3.
msc diagrams: three_way_teardown1(19) and call_teardown(5)
INCONSISTENCY:
Matching formula: m19 = m5
Precondition 1: rel (m19 , n19 , three_wayconnected k19);
Precondition 2: rel (m5 , n5 , connected);
Post condition 1: rel (n19 , k19 , connected);
Post condition 2: state (n5 , dial);

4.
msc diagrams: three_way_teardown2(16) and call_setup_failure2(9)
INCONSISTENCY:
Matching formula: k16 = m9
Precondition 1: rel (m16 , n16 , three_wayconnected k16);
Precondition 2: state (m9 , ringing n9);
Post condition 1: state (m16 , dial) & state (n16 , dial);
Post condition 2: state (n9 , idle);

5.
msc diagrams: three_way_teardown2(16) and call_teardown(5)
INCONSISTENCY:
Matching formula: k16 = m5
Precondition 1: rel (m16 , n16 , three_wayconnected k16);
Precondition 2: rel (m5 , n5 , connected);
Post condition 1: state (m16 , dial) & state (n16 , dial);
Post condition 2: state (n5 , dial);